class Proof(name: String, bufferDelay: Int, inputs: Theorem*) { // Some inputs tied to an and gate. Also there is a buffer.
  var delay = 0
  def this(name: String) { 
    this(name, 0) 
  }
  def this() { 
    this("unnamed")
  }
  def calcDelay():Int = inputs.foldLeft(0)( (a,b)=> a+b.delay ) + bufferDelay
  override def toString(): String = "Proof: " + name + " withDelay: " + calcDelay
}

class Theorem(name: String, methods: Proof*){ // this is the or gate. 这里的proof*实际上是多个uniq ID of the proof
  var delay = 1
  def this(name: String) { this(name, new Proof("commonSenseProof") ) }
  def this(){ this("unnamed") }

  def getAllMethods():String = methods.foldLeft("")( (a:String,b:Proof) => a + b + ";" )

  def calcDelay():Int = methods.foldLeft(0)( (a,b)=> a+b.delay ) -1

  override def toString(): String ={
    "Theorem " + name + "\n   has " + methods.length + " proofs withDelay: " + calcDelay + "\n"  + getAllMethods()
  }
}

object hello extends App {
  val t2 = new Theorem("haha2", new Proof("proof1"), new Proof("proof2") )
  println( t2 )

  val naiveTheorems = List(
    new Theorem("Seq has countably many elements"),
    new Theorem("We can choose subsequence"),
    new Theorem("There is a real/rational between two reals"),

    new Theorem("0 iff < epsilon"),
    new Theorem("Boundedness means sup and inf are reals"),
    new Theorem("Bounded infinity points has limit point"),

    new Theorem("Larger sets has bigger sup"),
    new Theorem("nothing")
  )

  naiveTheorems foreach println 

  val t1 = new Theorem("Subsequence of a bounded seq. is also ...", new Proof("proof1", 2,  naiveTheorems(6), naiveTheorems(4) ))
  println(t1)

}
